I'd like to wrap up first order inference today.

So the next thing we're going to go back to is this problem.

We have a true literal and a false literal in our branch.

Can I find a substitution that makes these two equal?

Right? Let me make an example.

f of g of x, y. Can I make this equal to f of z, h of c?

Can you?

It depends on your functions y and h. If there is an x for which...

Now x and y and z are variables. Is that your question?

No, I saw y was some kind of function.

No, y is...

I'll make little iota's to say those are individual variables.

Sorry, I took your g for a y.

So it's my fault after all, yes.

Then it depends on if you can find an x for which g of x equals z.

Yeah, can you?

It depends on g.

No, it doesn't.

You just take g of x for y.

That substitution makes... not y.

Almost.

g of x for z makes z and g of x equal.

If I drop in g of x here, then I have g of x here and g of x there.

That's not all we need.

You can continue.

Good.

On the right side, we do mostly the same.

We put y into h of z.

The other way around. You put terms into variables.

So h of z for y.

Now let's call that sigma.

And that makes those two equal, namely, both of these come b, f of g of x, h of z.

Okay?

Do you know another substitution that does this?

Is this the only solution?

Sigma is only the smallest solution we have.

There are infinitely many.

For example, we can substitute everything for a whole other function.

Concretely, can you dictate?

Another one.

We can only substitute variables, right?

Yes.

We can substitute c yoda by...

But c yoda is a constant.

You cannot substitute for that.

Substitute by, I mean...

Ah, substitute by c, yes.

So if I understand you correctly, you are proposing g of c for...

No, no, no, no.

The other c yoda in the right term.